Nuprl Lemma : rem_bounds_1
13,42
postcript
pdf
a
:
,
n
:
. (0
(
a
rem
n
)) & ((
a
rem
n
) <
n
)
latex
Up
int
2
,
int
2
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
False
,
P
Q
,
A
,
A
B
,
i
j
,
i
>
j
,
,
Lemmas
nat
wf
,
nat
plus
wf
origin
a:
, n:
. (0 
(a rem n)) & ((a rem n) < n) a:, n:. (0 (a rem n)) & ((a rem n) < n) 
Tx:A. B(x)
Q
A B
j